$\forall$$E$:Type, $x$, $y$:Tree($E$). tree\_node($<$$x$, $y$$>$) $\in$ Tree($E$)